es:event_system{i:l}, L:(Id List), del:rationals.
qless(0; del)
 fischer{x:ut2, try:ut2, taken:ut2, contending:ut2, free:ut2, mine:ut2, wanted:ut2, z:ut2}
 fischer(es; L)
 fischer-delay{i:l,
 fischer-delay{x:ut2,
 fischer-delay{try:ut2,
 fischer-delay{taken:ut2,
 fischer-delay{contending:ut2,
 fischer-delay{free:ut2,
 fischer-delay{mine:ut2,
 fischer-delay{wanted:ut2,
 fischer-delay{z:ut2}
 fischer-delay(es; del; L)
 (e,e':es-E(es).
 f-msg{wanted:ut2, free:ut2, z:ut2}
 f-msg(es; L; e)
  f-msg{wanted:ut2, free:ut2, z:ut2}
  f-msg(es; L; e')
  (es-sender(es; e') = es-sender(es; e)  es-E(es))
  qless(es-time(es; e'); (es-time(es; e) + del))) 

latex

Definitions	P  Q, True, T, P  Q, P  Q, prop{i:l}, guard(T), t  T, mkid{$x:ut2}, P  Q, P  Q, Id, x:A. B(x), x:A. B(x), fischer-delay, A c B, f-msg{$wanted:ut2, $free:ut2, $z:ut2}(es; L; e), fischer, subtype(S; T)
Lemmas	es-time-sender, mon ident q, qinverse q, qadd comm q, qadd ac 1 q, true wf, squash wf, qadd preserves qle, qmul wf, qle wf, iff transitivity, event system wf, Id wf, rationals wf, int inc rationals, qless wf, fischer wf, fischer-delay wf, es-E wf, f-msg wf, es-sender wf, qadd wf, es-time wf, qless transitivity 2 qorder, es-change-to wf